w-machine-independent(w;i;k;x)
== let Choose,Trans,Send = w-machine(w;i) in 
== s1, s2:(x:Idvartype(i;x)).
== (z:Id. z = x  s1(z) = s2(z))
==  (v:w-kindtype(w.TA(i);w.M;i)(k).
==  ((z:Id. z = x  Trans(k,v,s1,z) = Trans(k,v,s2,z)) & Send(k,v,s1) = Send(k,v,s2))
==  & (islocal(k)  Choose(act(k),s1) = Choose(act(k),s2)) 

latex

---

clarification:

w-machine-independent(w;i;k;x)
== let Choose,Trans,Send = w-machine(w;i) in 
== s1:(x:Idw-vartype(w; i; x)), s2:(x:Idw-vartype(w; i; x)).
== (z:Id. z = x  Id  s1(z) = s2(z)  w-vartype(w; i; z))
==  (v:w-kindtype(w.TA(i);w.M;i)(k).
==  ((z:Id. z = x  Id  Trans(k,v,s1,z) = Trans(k,v,s2,z)  w-vartype(w; i; z))
==  (& Send(k,v,s1) = Send(k,v,s2)  w-Msg(w) List)
==  & (islocal(k)
==  & ( Choose(act(k),s1) = Choose(act(k),s2)  w-kindtype(w.TA(i);w.M;i)(k)+Unit) 

latex

Definitions	let x,y,z = a in t(x;y;z), w-machine(w;i), x:AB(x), P & Q, x:A. B(x), A, Id, vartype(i;x), type List, Msg, P  Q, b, islocal(k), s = t, left+right, w-kindtype(TA;M;i), w.TA, w.M, Unit, f(a), act(k)
FDL editor aliases	w-machine-independent